a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
f2(a1(x), b) -> f2(b, a1(x))
↳ QTRS
↳ DependencyPairsProof
a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
f2(a1(x), b) -> f2(b, a1(x))
A1(a1(f2(b, a1(x)))) -> A1(a1(x))
A1(a1(x)) -> F2(a1(x), b)
A1(a1(x)) -> A1(f2(a1(x), b))
A1(a1(x)) -> F2(b, a1(f2(a1(x), b)))
A1(a1(f2(b, a1(x)))) -> A1(a1(a1(x)))
A1(a1(f2(b, a1(x)))) -> F2(a1(a1(a1(x))), b)
F2(a1(x), b) -> F2(b, a1(x))
a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
f2(a1(x), b) -> f2(b, a1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
A1(a1(f2(b, a1(x)))) -> A1(a1(x))
A1(a1(x)) -> F2(a1(x), b)
A1(a1(x)) -> A1(f2(a1(x), b))
A1(a1(x)) -> F2(b, a1(f2(a1(x), b)))
A1(a1(f2(b, a1(x)))) -> A1(a1(a1(x)))
A1(a1(f2(b, a1(x)))) -> F2(a1(a1(a1(x))), b)
F2(a1(x), b) -> F2(b, a1(x))
a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
f2(a1(x), b) -> f2(b, a1(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
A1(a1(f2(b, a1(x)))) -> A1(a1(x))
A1(a1(f2(b, a1(x)))) -> A1(a1(a1(x)))
a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
f2(a1(x), b) -> f2(b, a1(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A1(a1(f2(b, a1(x)))) -> A1(a1(x))
Used ordering: Polynomial interpretation [21]:
A1(a1(f2(b, a1(x)))) -> A1(a1(a1(x)))
POL(A1(x1)) = 1 + x1
POL(a1(x1)) = 1 + x1
POL(b) = 0
POL(f2(x1, x2)) = x1 + x2
a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
f2(a1(x), b) -> f2(b, a1(x))
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
A1(a1(f2(b, a1(x)))) -> A1(a1(a1(x)))
a1(a1(f2(b, a1(x)))) -> f2(a1(a1(a1(x))), b)
a1(a1(x)) -> f2(b, a1(f2(a1(x), b)))
f2(a1(x), b) -> f2(b, a1(x))